/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;


/** One Boolean literal: variable or its negation.  Uses flywheel pattern: single GBF_Lit shared for each literal
    among all uses. */
class GBF_Lit extends BooleanFormula {
    private int _lit;

    int getNumVars() { return Math.abs(_lit); }

    protected boolean checkConstantValued() { return false; }
	
    /** Positive literals that are shared.  Array is expanded as needed.
	Invariant: _posLit[i].lit == i+1.*/
    private static GBF_Lit[] _posLit; // = _ensureSize(new GBF_Lit[]{}, 128, +1);
    /** Negative literals that are shared.  Array is expanded as needed.
	Invariant: _negLit[i].lit == -(i+1).*/
    private static GBF_Lit[] _negLit; // = _ensureSize(new GBF_Lit[]{}, 128, -1);

    public static void initSingletons() {
    	_posLit = null;
    	_negLit = null;
    	_posLit = _ensureSize(new GBF_Lit[]{}, 128, +1);
    	_negLit = _ensureSize(new GBF_Lit[]{}, 128, -1);
    }
    
    private GBF_Lit(int lit_) { this._lit = lit_; }

    /** Return the literal */
    int getLit() { return _lit; }

    /** Return the opposite literal */
    GBF_Lit opposite() { return getLitObj(-_lit); }

    public String toString() { return Integer.toString(_lit); }

    protected Object handleVisitor(GBF_V visitor_) { return visitor_.forLit(this); }

    static GBF_Lit getLitObj(int lit) {
	int var = Math.abs(lit);
	
	if (lit > 0) { _posLit = _ensureSize(_posLit, var, +1); return _posLit[var-1]; }
	else if (lit < 0) { _negLit = _ensureSize(_negLit, var, -1); return _negLit[var-1]; }
	else throw new Error("getLitObj: invalid zero literal");
    }
    
    private static GBF_Lit[] _ensureSize(GBF_Lit[] lits_, int size_, int mult_) {
	if (lits_.length >= size_) return lits_;
	GBF_Lit[] newLits = new GBF_Lit[Math.max(size_, lits_.length * 2)];
	System.arraycopy(lits_, 0, newLits, 0, lits_.length);
	for (int i=lits_.length; i < newLits.length; i++) {
	    newLits[i] = new GBF_Lit((i+1) * mult_);
	}
	return newLits;
    }

    /**
     * Simplify this boolean formula using the given partial assignment.
     * Return a reference to the simplified version of the boolean formula
     * (recall that {@link BooleanFormula}s are immutable).  This method
     * provides a more efficient implementation than {@link BooleanFormula#simplify}.
     */
    public BooleanFormula simplify(PartialAssignment pa_) {
	int var = _lit>0 ? _lit : -_lit;
	return pa_.isAssigned(var) ?
	    BooleanFormula.makeConst(pa_.getLitValue(_lit)) : this;
    }
}
